A Complete Axiomatization of Strict Equality
Identifieur interne : 003145 ( Main/Exploration ); précédent : 003144; suivant : 003146A Complete Axiomatization of Strict Equality
Auteurs : Javier Álvez [Espagne] ; Francisco J. L Pez-Fraguas [Espagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Computing with data values that are some kind of trees —finite, infinite, rational— is at the core of declarative programming, either logic, functional, or functional-logic. Understanding the logic of trees is therefore a fundamental question with impact in different aspects, like language design, including constraint systems or constructive negation, or obtaining methods for verifying and reasoning about programs. The theory of true equality over finite or infinite trees is quite well-known. In particular, a seminal paper by Maher proved its decidability and gave a complete axiomatization of the theory. However, the sensible notion of equality for functional and functional-logic languages with a lazy evaluation regime is strict equality, a computable approximation of true equality for possibly infinite and partial trees. In this paper, we investigate the first-order theory of strict equality, arriving to remarkable and not obvious results: the theory is again decidable and admits a complete axiomatization, not requiring predicate symbols other than strict equality itself. Besides, the results stem from an effective —taking into account the intrinsic complexity of the problem— decision procedure that can be seen as a constraint solver for general strict equality constraints. As a side product of our results, we obtain that the theories of strict equality over finite and infinite partial trees, respectively, are elementarily equivalent.
Url:
DOI: 10.1007/978-3-642-12251-4_10
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000386
- to stream Istex, to step Curation: 000384
- to stream Istex, to step Checkpoint: 000907
- to stream Main, to step Merge: 003202
- to stream Main, to step Curation: 003145
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Complete Axiomatization of Strict Equality</title><author><name sortKey="Alvez, Javier" sort="Alvez, Javier" uniqKey="Alvez J" first="Javier" last="Álvez">Javier Álvez</name></author><author><name sortKey="L Pez Fraguas, Francisco J" sort="L Pez Fraguas, Francisco J" uniqKey="L Pez Fraguas F" first="Francisco J." last="L Pez-Fraguas">Francisco J. L Pez-Fraguas</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:1108F8810C029FF3697E3BB2F5BC383155979051</idno><date when="2010" year="2010">2010</date><idno type="doi">10.1007/978-3-642-12251-4_10</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-8XHWD5PC-W/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000386</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000386</idno><idno type="wicri:Area/Istex/Curation">000384</idno><idno type="wicri:Area/Istex/Checkpoint">000907</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000907</idno><idno type="wicri:doubleKey">0302-9743:2010:Alvez J:a:complete:axiomatization</idno><idno type="wicri:Area/Main/Merge">003202</idno><idno type="wicri:Area/Main/Curation">003145</idno><idno type="wicri:Area/Main/Exploration">003145</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Complete Axiomatization of Strict Equality</title><author><name sortKey="Alvez, Javier" sort="Alvez, Javier" uniqKey="Alvez J" first="Javier" last="Álvez">Javier Álvez</name><affiliation wicri:level="4"><orgName type="university">Université complutense de Madrid</orgName><country>Espagne</country><placeName><settlement type="city">Madrid</settlement><region nuts="2" type="region">Communauté de Madrid</region></placeName></affiliation><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation></author><author><name sortKey="L Pez Fraguas, Francisco J" sort="L Pez Fraguas, Francisco J" uniqKey="L Pez Fraguas F" first="Francisco J." last="L Pez-Fraguas">Francisco J. L Pez-Fraguas</name><affiliation wicri:level="4"><orgName type="university">Université complutense de Madrid</orgName><country>Espagne</country><placeName><settlement type="city">Madrid</settlement><region nuts="2" type="region">Communauté de Madrid</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Computing with data values that are some kind of trees —finite, infinite, rational— is at the core of declarative programming, either logic, functional, or functional-logic. Understanding the logic of trees is therefore a fundamental question with impact in different aspects, like language design, including constraint systems or constructive negation, or obtaining methods for verifying and reasoning about programs. The theory of true equality over finite or infinite trees is quite well-known. In particular, a seminal paper by Maher proved its decidability and gave a complete axiomatization of the theory. However, the sensible notion of equality for functional and functional-logic languages with a lazy evaluation regime is strict equality, a computable approximation of true equality for possibly infinite and partial trees. In this paper, we investigate the first-order theory of strict equality, arriving to remarkable and not obvious results: the theory is again decidable and admits a complete axiomatization, not requiring predicate symbols other than strict equality itself. Besides, the results stem from an effective —taking into account the intrinsic complexity of the problem— decision procedure that can be seen as a constraint solver for general strict equality constraints. As a side product of our results, we obtain that the theories of strict equality over finite and infinite partial trees, respectively, are elementarily equivalent.</div></front></TEI><affiliations><list><country><li>Espagne</li></country><region><li>Communauté de Madrid</li></region><settlement><li>Madrid</li></settlement><orgName><li>Université complutense de Madrid</li></orgName></list><tree><country name="Espagne"><region name="Communauté de Madrid"><name sortKey="Alvez, Javier" sort="Alvez, Javier" uniqKey="Alvez J" first="Javier" last="Álvez">Javier Álvez</name></region><name sortKey="Alvez, Javier" sort="Alvez, Javier" uniqKey="Alvez J" first="Javier" last="Álvez">Javier Álvez</name><name sortKey="Alvez, Javier" sort="Alvez, Javier" uniqKey="Alvez J" first="Javier" last="Álvez">Javier Álvez</name><name sortKey="L Pez Fraguas, Francisco J" sort="L Pez Fraguas, Francisco J" uniqKey="L Pez Fraguas F" first="Francisco J." last="L Pez-Fraguas">Francisco J. L Pez-Fraguas</name><name sortKey="L Pez Fraguas, Francisco J" sort="L Pez Fraguas, Francisco J" uniqKey="L Pez Fraguas F" first="Francisco J." last="L Pez-Fraguas">Francisco J. L Pez-Fraguas</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003145 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003145 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:1108F8810C029FF3697E3BB2F5BC383155979051
|texte= A Complete Axiomatization of Strict Equality
}}
| This area was generated with Dilib version V0.6.33. |  |